#!/usr/bin/env ruby

class String
    def begins?(s)
        self[0...(s.size)] == s
    end

    def ends?(s)
        self[(self.size - s.size)...(self.size)] == s
    end
end

HEADER = <<-eos
-- Train-Gate-Controller with faulty trains
-- Number of trains = $NUMBER_OF_TRAINS$
-- Overall Counter = $OVERALL_COUNTER$
-- Depth of break = $BREAK_DEPTH$

eos


TRAIN_VAR_ADD = "        train$TRAIN_NUMBER$_waiting : boolean;\n"
TRAIN_ACTION_ADD = "    Actions = { $TRAIN_ACTIONS$idle };" 
TRAIN_PROT_ADD = "        lights = green and train$TRAIN_NUMBER$_waiting = true : { enter$TRAIN_NUMBER$ };\n"
TRAIN_EVOL_ENTER_ADD = "        lights = red and train$TRAIN_NUMBER$_waiting = false if train$TRAIN_NUMBER$_waiting = true and lights = green and Action = enter$TRAIN_NUMBER$ and Train$TRAIN_NUMBER$.Action = enter;\n"
TRAIN_EVOL_SIGNAL_ADD = "        train$TRAIN_NUMBER$_waiting = true if Action = idle and Train$TRAIN_NUMBER$.Action = signal;\n"


ENVIRONMENT = <<-eos
Agent Environment
    Vars:
        lights : { red, green };

$TRAIN_VAR$
        counter : 0..2;
    end Vars
    
$TRAIN_ACTION$

    Protocol:

$TRAIN_PROT$
        Other: { idle };
    end Protocol
    
    Evolution:
        counter = counter + 1 if counter < 2 and lights = red;
        
        lights = green and counter = 0 if counter = 2 and lights = red;
        
$TRAIN_EVOL_ENTER$ 
$TRAIN_EVOL_SIGNAL$       
    end Evolution

end Agent

eos

AGENT_ADD = <<-eos
Agent Train$TRAIN_NUMBER$
    
    Vars:
        state : { wait, tunnel, away };
        serviced : 0..$TOTAL_COUNT$;
        broken : boolean;
    end Vars

    Actions = { signal, enter, leave, back, service, break };
    
    Protocol:
        serviced = $TOTAL_COUNT$ and (state = away or state = wait) : { service };
        state = wait and serviced < $TOTAL_COUNT$ : { signal, service, enter };
        
        -- Trains work correctly if the non-deterministic break action is removed 
        -- Replace the following lines:
        $TRAIN_BROKEN$state = tunnel and serviced < $BREAK_COUNT$ and broken = false: { leave };
        $TRAIN_BROKEN$state = tunnel and serviced >= $BREAK_COUNT$ and serviced < $TOTAL_COUNT$ and broken = false : { leave, break };
        $TRAIN_BROKEN$state = tunnel and broken = true : { break };
        $TRAIN_BROKEN$state = tunnel and serviced = $TOTAL_COUNT$ and broken = false : { break };
        -- With:
        $TRAIN_WORKING$state = tunnel : { leave };
        
        state = away and serviced < $TOTAL_COUNT$ : { service, back };
    end Protocol
    
    Evolution:
        serviced = 0 if Action = service;

        state = tunnel if broken = true and state = tunnel;
        state = tunnel and broken = true if state = tunnel and Action = break;
        state = wait and serviced = serviced + 1 if serviced < $TOTAL_COUNT$ and state = wait and Action = signal;
        state = wait and serviced = serviced + 1 if serviced < $TOTAL_COUNT$ and state = away and Action = back;
        state = tunnel and serviced = serviced + 1 if serviced < $TOTAL_COUNT$ and state = wait and Action = enter and Environment.Action = enter$TRAIN_NUMBER$;
        state = away and serviced = serviced + 1 if serviced < $TOTAL_COUNT$ and state = tunnel and Action = leave;
        
        -- The only edge case is that the train cannot be serviced in the tunnel
        state = away and serviced = $TOTAL_COUNT$ if serviced = $TOTAL_COUNT$ and state = tunnel and Action = leave;
    end Evolution

end Agent

eos

TRAIN_EVAL_ADD = "    train$TRAIN_NUMBER$_in_tunnel if Train$TRAIN_NUMBER$.state = tunnel;\n"

EVALUATION = <<-eos
Evaluation

$TRAIN_EVAL$
end Evaluation

eos

INIT_ADD = <<-eos
        Environment.train$TRAIN_NUMBER$_waiting = false and
        Train$TRAIN_NUMBER$.state = away and
        Train$TRAIN_NUMBER$.serviced = 0 and
        Train$TRAIN_NUMBER$.broken = false and\n
eos


INIT_STATES = <<-eos
InitStates
    Environment.lights = green and

$INIT_ADD$
        Environment.counter = 0; 
end InitStates
eos

#    -- AG(EF(train$TRAIN_NUMBER$_in_tunnel));

TRAIN_FORMULAE_SINGLE = <<-eos
    --AG(AF(!train$TRAIN_NUMBER$_in_tunnel));

eos

TRAIN_FORMULAE_PAIR = <<-eos
    --AG((!train$ID_ONE$_in_tunnel or !train$ID_TWO$_in_tunnel));

eos

TRAIN_FORMULAE_KNOWLEDGE_SINGLE = <<-eos
    --AG(train$ID_ONE$_in_tunnel -> K(Train$ID_ONE$, (!train$ID_TWO$_in_tunnel)));

eos

TRAIN_FORMULAE_KNOWLEDGE_PAIR = <<-eos
    --AG(K(Train$ID_ONE$, (!train$ID_ONE$_in_tunnel or !train$ID_TWO$_in_tunnel)));

eos

TRAIN_FORMULAE_KNOWLEDGE_NEXT = <<-eos
    --AG(train$ID_ONE$_in_tunnel -> K(Train$ID_ONE$, AX($TRAINS$)));

eos

FORMULAE = <<-eos
Formulae
    
    -- On all paths, there always exists a time in which the train is no longer in the tunnel.
$TRAIN_FORMULAE_SINGLE$
    
    -- On all paths, either Train1 isn't the tunnel, or Train2 isn't in the tunnel, or neither of them are
    -- This really checks that two trains aren't in the tunnel at the same time
$TRAIN_FORMULAE_PAIR$
    
    -- When a train is in the tunnel, then it knows that another train isn't in the tunnel
$TRAIN_FORMULAE_KNOWLEDGE_SINGLE$
    
    -- Trains always know that they have exclusive use of the tunnel
$TRAIN_FORMULAE_KNOWLEDGE_PAIR$

    -- Trains know that the controller takes an extra turn to allow the next train to enter
    -- Therefore, the train knows that there will not be another train in the tunnel in the next state
$TRAIN_FORMULAE_KNOWLEDGE_NEXT$
    
end Formulae
eos


if __FILE__ == $0 then

count = 2
countermax = 100
counterbreak = 75
working = "-- "
broken = ""

if ARGV.size >= 3
    count = ARGV[0].to_i
    countermax = ARGV[1].to_i
    counterbreak = ARGV[2].to_i
end

if ARGV.size >= 4
    if ARGV[3] == "w"
        working = ""
        broken = "-- "
    end
end

puts HEADER.gsub(/\$NUMBER_OF_TRAINS\$/, sprintf("%d",count)).gsub(/\$OVERALL_COUNTER\$/, sprintf("%d",countermax)).gsub(/\$BREAK_DEPTH\$/, sprintf("%d",counterbreak))

varadd = String.new
actionadd = String.new
protadd = String.new
evolenteradd = String.new
evolsignaladd = String.new

for i in 1..count do
   varadd += TRAIN_VAR_ADD.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
   protadd += TRAIN_PROT_ADD.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
   evolenteradd += TRAIN_EVOL_ENTER_ADD.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
   evolsignaladd += TRAIN_EVOL_SIGNAL_ADD.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
   actionadd += sprintf("enter%d, ",i)
end

environment = ENVIRONMENT.gsub(/\$TRAIN_VAR\$/, varadd)
actionadd = TRAIN_ACTION_ADD.gsub(/\$TRAIN_ACTIONS\$/, actionadd)
environment = environment.gsub(/\$TRAIN_PROT\$/, protadd)
environment = environment.gsub(/\$TRAIN_EVOL_ENTER\$/, evolenteradd)
environment = environment.gsub(/\$TRAIN_EVOL_SIGNAL\$/, evolsignaladd)
environment = environment.gsub(/\$TRAIN_ACTION\$/,actionadd)

puts environment

for i in 1..count do
    current_agent = ""
    current_agent = AGENT_ADD.gsub(/\$TOTAL_COUNT\$/, sprintf("%d", countermax))
    current_agent = current_agent.gsub(/\$BREAK_COUNT\$/, sprintf("%d", counterbreak))
    current_agent = current_agent.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d", i))
    current_agent = current_agent.gsub(/\$TRAIN_BROKEN\$/, broken)
    current_agent = current_agent.gsub(/\$TRAIN_WORKING\$/, working)

    puts current_agent
end

evaladd = String.new
for i in 1..count do
    evaladd += TRAIN_EVAL_ADD.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
end

evaluation = EVALUATION.gsub(/\$TRAIN_EVAL\$/, evaladd)
puts evaluation

initadd = String.new
for i in 1..count do
    initadd += INIT_ADD.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
end

initstates = INIT_STATES.gsub(/\$INIT_ADD\$/, initadd)
puts initstates

test = false
formulae_add_single = String.new
for i in 1..count do
    if test
        formulae_add_single += TRAIN_FORMULAE_SINGLE.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i)).gsub(/--/,'')
        test = false
    else
        formulae_add_single += TRAIN_FORMULAE_SINGLE.gsub(/\$TRAIN_NUMBER\$/, sprintf("%d",i))
    end
end

formulae_add_pair = String.new
for i in 1..count do
    for j in i..count do
        if i != j
            formulae_add_pair += TRAIN_FORMULAE_PAIR.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$ID_TWO\$/, sprintf("%d",j))
        end
    end
end

formulae_add_knowledge_single = String.new
for i in 1..count do
    for j in 1..count do
        if i != j
            formulae_add_knowledge_single += TRAIN_FORMULAE_KNOWLEDGE_SINGLE.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$ID_TWO\$/, sprintf("%d",j))
        end
    end
end

formulae_add_knowledge_pair = String.new
for i in 1..count do
    for j in 1..count do
        if i != j
            formulae_add_knowledge_pair += TRAIN_FORMULAE_KNOWLEDGE_PAIR.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$ID_TWO\$/, sprintf("%d",j))
        end
    end
end

formulae_add_knowledge_next = String.new
string = String.new
for i in 1..count do
    string += sprintf("!train%d_in_tunnel or ",i)
end

test = true
tempstr = string
for i in 1..count do
    temp = sprintf("!train%d_in_tunnel or ",i)
    string = string.gsub(/#{temp}/,'')    
    string = string.slice(0,string.length - 4)
    
    if test
        formulae_add_knowledge_next += TRAIN_FORMULAE_KNOWLEDGE_NEXT.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$TRAINS\$/, string).gsub(/--/,'')
        test = false
    else
        formulae_add_knowledge_next += TRAIN_FORMULAE_KNOWLEDGE_NEXT.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$TRAINS\$/, string)
    end
    string = tempstr
end

=begin
test = true
for i in 1..count do
    for j in 1..count do
        if i != j
            if test
                formulae_add_knowledge_next += TRAIN_FORMULAE_KNOWLEDGE_NEXT.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$ID_TWO\$/, sprintf("%d",j)).gsub(/--/,'')
                test = false
            else
                formulae_add_knowledge_next += TRAIN_FORMULAE_KNOWLEDGE_NEXT.gsub(/\$ID_ONE\$/, sprintf("%d",i)).gsub(/\$ID_TWO\$/, sprintf("%d",j))
            end
        end
    end
end
=end

formulae = FORMULAE.gsub(/\$TRAIN_FORMULAE_SINGLE\$/, formulae_add_single)
formulae = formulae.gsub(/\$TRAIN_FORMULAE_PAIR\$/, formulae_add_pair)
formulae = formulae.gsub(/\$TRAIN_FORMULAE_KNOWLEDGE_SINGLE\$/, formulae_add_knowledge_single)
formulae = formulae.gsub(/\$TRAIN_FORMULAE_KNOWLEDGE_PAIR\$/, formulae_add_knowledge_pair)
formulae = formulae.gsub(/\$TRAIN_FORMULAE_KNOWLEDGE_NEXT\$/, formulae_add_knowledge_next)
puts formulae

end
